Nuprl Lemma : R-state-var-loc 11,40

ds,da,x,T:top, ks:(top List), tr:top, j,i:Id.
sqequal(R-has-loc(R-state-var(idsdaxTkstr); j); eq_id(ij)) 
latex


DefinitionsY, if b then t else f fi , prop{i:l}, tt, P  Q, ff, reduce(fkas), bor(pq), xt(x), t  T, R-state-var(idsdaxTkstr), R-has-loc(Ri), top, x:AB(x), guard(T), sq_type(T), P  Q, P  Q, Unit, , x(s),
Lemmasbool sq, bfalse wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, btrue wf, assert-eq-id, eqtt to assert, assert wf, iff transitivity, bool wf, eq id wf, top wf, Id wf, Rall-has-loc

origin